Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    le(0,Y)  → true
2:    le(s(X),0)  → false
3:    le(s(X),s(Y))  → le(X,Y)
4:    app(nil,Y)  → Y
5:    app(cons(N,L),Y)  → cons(N,app(L,Y))
6:    low(N,nil)  → nil
7:    low(N,cons(M,L))  → iflow(le(M,N),N,cons(M,L))
8:    iflow(true,N,cons(M,L))  → cons(M,low(N,L))
9:    iflow(false,N,cons(M,L))  → low(N,L)
10:    high(N,nil)  → nil
11:    high(N,cons(M,L))  → ifhigh(le(M,N),N,cons(M,L))
12:    ifhigh(true,N,cons(M,L))  → high(N,L)
13:    ifhigh(false,N,cons(M,L))  → cons(M,high(N,L))
14:    quicksort(nil)  → nil
15:    quicksort(cons(N,L))  → app(quicksort(low(N,L)),cons(N,quicksort(high(N,L))))
There are 15 dependency pairs:
16:    LE(s(X),s(Y))  → LE(X,Y)
17:    APP(cons(N,L),Y)  → APP(L,Y)
18:    LOW(N,cons(M,L))  → IFLOW(le(M,N),N,cons(M,L))
19:    LOW(N,cons(M,L))  → LE(M,N)
20:    IFLOW(true,N,cons(M,L))  → LOW(N,L)
21:    IFLOW(false,N,cons(M,L))  → LOW(N,L)
22:    HIGH(N,cons(M,L))  → IFHIGH(le(M,N),N,cons(M,L))
23:    HIGH(N,cons(M,L))  → LE(M,N)
24:    IFHIGH(true,N,cons(M,L))  → HIGH(N,L)
25:    IFHIGH(false,N,cons(M,L))  → HIGH(N,L)
26:    QUICKSORT(cons(N,L))  → APP(quicksort(low(N,L)),cons(N,quicksort(high(N,L))))
27:    QUICKSORT(cons(N,L))  → QUICKSORT(low(N,L))
28:    QUICKSORT(cons(N,L))  → LOW(N,L)
29:    QUICKSORT(cons(N,L))  → QUICKSORT(high(N,L))
30:    QUICKSORT(cons(N,L))  → HIGH(N,L)
The approximated dependency graph contains 5 SCCs: {17}, {16}, {22,24,25}, {18,20,21} and {27,29}. Hence the TRS is terminating.
Tyrolean Termination Tool  (0.85 seconds)   ---  May 3, 2006